Inference at * 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. i : {0..(||L1 @ L2|| - 1)}
7. x = (L1 @ L2)[i]
8. y = (L1 @ L2)[(i+1)]
  (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
   ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
   (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)])) 

latex

 by ((Decide i < ||L1||) 
CollapseTHENA (Auto)) 

latex

C1: 

C1: 9. i < ||L1||
C1:   (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
C1:    ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
C1:    (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)]))
C2: 

C2: 9. (i < ||L1||)
C2:   (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
C2:    ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
C2:    (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)]))
C.

Definitions	a < b, ||as||, (xL.P(x)), xL. P(x), x f y, f(a), A c B, a < b, a <p b, a  b, a ~ b, b | a, x:A. B(x), x:A  B(x), P  Q, b, s = t, A  B, x:A. B(x), x:AB(x), Dec(P), P  Q, left + right
Lemmas	decidable lt